(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const i7 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i13 Int)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r9 Real)
(declare-const r11 Real)
(declare-const r12 Real)
(assert (xor v10 v3 v2 v8))
(declare-const arr-6714223472513213107_-4902517508123168358-0 (Array Real Bool))
(assert (xor (xor v10 v3 v2 v8) (distinct 181.0 r6 r12 565.0 4881.0)))
(declare-const _17-0 (_ BitVec 17))
(declare-const arr--244189969488280568_-244189969488280568-0 (Array (Array Real Bool) (Array Real Bool)))
(push)
(declare-const v18 Bool)
(declare-const arr--4835957693419374033_-244189969488280568-0 (Array (_ BitVec 17) (Array Real Bool)))
(assert (not (exists ((q0 Bool) (q1 (Array Real Bool)) (q2 (Array Real Bool)) (q3 Bool)) (=> (not (= (distinct 181.0 r6 r12 565.0 4881.0) v11 v5 (= arr-6714223472513213107_-4902517508123168358-0 arr-6714223472513213107_-4902517508123168358-0) (is_int r9) v5)) (= q2 arr-6714223472513213107_-4902517508123168358-0 q2)))))
(assert (or (forall ((q0 Bool) (q1 (Array Real Bool)) (q2 (Array Real Bool)) (q3 Bool)) (=> (select q2 181.0) (xor q0 (= _17-0 _17-0 _17-0 _17-0)))) (exists ((q0 Bool) (q1 (Array Real Bool)) (q2 (Array Real Bool)) (q3 Bool)) (not (distinct q3 q0 q3)))))
(check-sat)
